x:chain_config(). (ccsucc?(x))  (ccsucc-id(x)  Id) 

latex

Definitions	s = t, t  T, True, Id, , x:AB(x), P  Q, chain config ind ccsucc compseq tag def, b, ccsucc?(x), ccsucc-id(x), False, chain config ind ccpred compseq tag def, chain config ind cctail compseq tag def, #$n, , Type, , chain config ind cchead compseq tag def, x:A  B(x), left + right, Unit, chain_config(), x:A. B(x)
Lemmas	Id wf, member wf, assert wf, chain config wf, false wf, true wf